\begin{tabbing}
R{-}interface{-}compat($A$; $B$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if Rsends?($B$)\+
\\[0ex]then \=if\= Reffect?($A$)\+\+
\\[0ex]then let \=$k$\= = Reffect{-}knd($A$) in\+\+
\\[0ex]if band(isrcv($k$); eq\_lnk(lnk($k$); Rsends{-}l($B$)))
\-\\[0ex]then subtype\_rel(\=fpf{-}cap(Rsends{-}dt($B$); id{-}deq; tag($k$); void);\+
\\[0ex]Reffect{-}T($A$))
\-\\[0ex]else True
\\[0ex]fi 
\-\-\\[0ex]if\= Rsends?($A$)\+
\\[0ex]then let \=$k$\= = Rsends{-}knd($A$) in\+\+
\\[0ex]if band(isrcv($k$); eq\_lnk(lnk($k$); Rsends{-}l($B$)))
\-\\[0ex]then subtype\_rel(\=fpf{-}cap(Rsends{-}dt($B$); id{-}deq; tag($k$); void);\+
\\[0ex]Rsends{-}T($A$))
\-\\[0ex]else True
\\[0ex]fi 
\-\-\\[0ex]else True
\\[0ex]fi 
\-\\[0ex]else True
\\[0ex]fi 
\-
\end{tabbing}